public class HashTable {
	//@ invariant containsDoubleObject == false;
	//@ invariant isCorrectIndex == true;

	private/*@ pure @*/ boolean containsDoubleObject(){
		EntryList eList;
		for(int i = 0; i < arr.length;i++){
			if(arr[i] != null){
				eList = arr[i];
				do{
					for(int j = i + 1; j < arr.length;j++){
						if(arr[j] != null && arr[j].contains(eList.first)){
							return true;
						}
					}
					if(eList.rest != null && eList.rest.contains(eList.first)){
						return true;
					}
					eList=eList.rest;
				}while(eList != null);
			}
		}
		return false;
	}
	
	private/*@ pure @*/ boolean isCorrectIndex(){
		EntryList eList;
		for(int i = 0; i < arr.length;i++){
			if(arr[i] != null){
				eList = arr[i];
				do{
					int ix = Math.abs(eList.first.hashCode() % arr.length);
					if(ix != i){
						return false;
					}
					eList=eList.rest;
				}while(eList != null);
			}
		}
		return true;
	}

	/*@ spec_public @*/ EntryList[] arr;
	/*@ spec_public @*/ int size;

	/* A simple linked list of entries.
	 */
	private class EntryList {
		Object first;
		EntryList rest;

		EntryList( Object first, EntryList rest ) {
			this.first = first;
			this.rest = rest;
		}
		
		public /*@ pure @*/ boolean contains(Object ob){
			if(ob == null){
				return false;
			}
			for (EntryList entLi = this; entLi != null; entLi = entLi.rest )
				if ( entLi.first.equals( ob ) )
					return true;
			return false;
		}
	}

	/* Creates an empty HashTable with an array of length init.
	 */
	public HashTable( int init ) {
		arr = new EntryList[init];
		size = 0;
	}

	/* Returns the size.
	 */
	//@ public normal_behavior
	//@ ensures \result == size;
	//@ assignable \nothing;
	public int getSize() {
		return size;
	}

	/* Adds x to the hashtable
	 */
	//@ public normal_behavior
	//@ requires this.contains(x);
	//@ ensures \old(size) == size;
	//@ also
	//@ public normal_behavior
	//@ requires !this.contains(x);
	//@ ensures size == \old(size)+1;
	//@ ensures this.contains(x);
	//@ assignable arr[*], size;
	public void add( Object x ) {

		int ix = Math.abs(x.hashCode() % arr.length);
		EntryList entLi = arr[ix];

		if ( entLi != null ) {
			while ( entLi.rest != null ) {
				if ( entLi.first.equals( x ) )
					return;
				entLi = entLi.rest;
			}
			entLi.rest = new EntryList(x,null);
		}
		else
			arr[ix] = new EntryList(x,null);

		size++;
	}

	/* Checks if x is in the hashtable.
	 */
	//@ public normal_behavior
	//@ requires (\exists int i; i >= 0 && i < arr.length; arr[i].contains(x)==true);
	//@ ensures \result == true;
	//@ also
	//@ public normal_behavior
	//@ requires (\forall int i; i >= 0 && i < arr.length; arr[i].contains(x)==false);
	//@ ensures \result == false;
	public /*@ pure @*/ boolean contains( Object x ) {

		int ix = Math.abs(x.hashCode()) % arr.length;

		for ( EntryList entLi = arr[ix]; entLi != null; entLi = entLi.rest )
			if ( entLi.first.equals( x ) )
				return true;

		return false;

	}

	/* Removes x from the hashtable.
	 */
	//@ public normal_behavior
	//@ requires this.contains(x);
	//@ ensures size == \old(size)-1;
	//@ ensures !this.contains(x);
	//@ assignable size;
	//@ also
	//@ public normal_behavior
	//@ requires !this.contains(x);
	//@ ensures size == \old(size);
	public void remove( Object x ) {

		int ix = Math.abs(x.hashCode() % arr.length);
		EntryList entLi = arr[ix];

		if ( entLi != null ) {
			while ( entLi.rest != null ) {
				if ( entLi.rest.first.equals( x ) ) {
					entLi.rest = entLi.rest.rest;
					size--;
					return;
				}
				entLi = entLi.rest;
			}
		}
	}

}
